Nuprl Lemma : Rall_wf
11,40
postcript
pdf
T
:Type,
L
:(
T
List),
R
:({
x
:
T
| (
x
L
)}
es_realizer{i:l}). Rall(
L
;
x
.
R
(
x
))
es_realizer{i:l}
latex
Definitions
x
(
s
)
,
Rall(
L
;
x
.
R
(
x
))
,
t
T
,
x
:
A
.
B
(
x
)
,
prop{i:l}
Lemmas
l
member
wf
,
es
realizer
wf
,
map-wf2
,
Rlist
wf
origin
T:Type, L:(T List), R:({x:T| (x 
L)} 
es_realizer{i:l}). Rall(L; x.R(x)) es_realizer{i:l} T:Type, L:(T List), R:({x:T| (x L)} es_realizer{i:l}). Rall(L; x.R(x)) es_realizer{i:l} Tx:A. B(x)